

open Ast
open Cub
open Mods

let types = Hashtbl.create 32 (* (id, type_expr) *)
let vars = Hashtbl.create 32 (* (id,  type_expr) *)
let funs = Hashtbl.create 32 (* (id,  (type_expr, type_expr StrMap.t) ) *)

let mk_node e t = {data = t; node = e}

(*
let mt2cubt = function
  | Tident (id) -> () (* failwith "TODO" *)
  | Tsubrange (i1, i2) -> () (* failwith "TODO" *)
  | Tenum (idl) -> () (* failwith "TODO" *)
  | Trecord (vdl) -> () (* failwith "TODO" *)
  | Tarray (te1, te2) -> () (* failwith "TODO" *)
  | Tscalarset i -> () (* failwith "TODO" *)
  | Tunion te -> () (* failwith "TODO" *)
  | Tmultiset (e, te) -> () (* failwith "TODO" *)
  | Tint -> () (* failwith "TODO" *)
  | Tany -> () (* failwith "TODO" *)
*)
  
let loc_dummy e =
  mk_node e (Lexing.dummy_pos, Lexing.dummy_pos)

let rec compile_quantif q =
  match q.node with
  | Qvar (id, te) -> () (* failwith "TODO" *)
  | Qfor (id, e1, e2, e3) -> () (* failwith "TODO" *)

and compile_quantifs ql =
  List.map compile_quantif ql

and compile_desig designator =
  match designator.node with
  | DESid id -> () (* failwith "TODO" *)
  | DESarray (d, e) -> () (* failwith "TODO" *)
  | DESdot (d, id) -> () (* failwith "TODO" *)

and compile_stmt stmt =
  match stmt.node with
  | Sassign (d, e) -> () (* failwith "TODO" *)
  | Sif (e, sl1, sl2) -> () (* failwith "TODO" *)
  | Sswitch (e, esl, sl) -> () (* failwith "TODO" *)
  | Sfor (ql, sl) -> () (* failwith "TODO" *)
  | Swhile (e, sl) -> () (* failwith "TODO" *)
  | Salias (al, sl) -> () (* failwith "TODO" *)
  | Sproccall (id, el) -> () (* failwith "TODO" *)
  | Sundef d -> () (* failwith "TODO" *)
  | Serror s -> () (* failwith "TODO" *)
  | Sclear d -> () (* failwith "TODO" *)
  | Sassert (e, os) -> () (* failwith "TODO" *)
  | Sput (Putexpr pe) -> () (* failwith "TODO" *)
  | Sput (Putstring s) -> () (* failwith "TODO" *)
  | Sreturn (None) -> () (* failwith "TODO" *)
  | Sreturn (Some e) -> () (* failwith "TODO" *)
  | Smultisetadd (d1, d2) -> () (* failwith "TODO" *)
  | Smultisetremovepred (id, d, e) -> () (* failwith "TODO" *)
  | Smultisetremove (e, d) -> () (* failwith "TODO" *)

and compile_stmts sl =
  List.map compile_stmt sl

and compile_expr e =
  match e.node with
  | Eforall (ql, e) -> () (* failwith "TODO" *)
  | Eexists (ql, e) -> () (* failwith "TODO" *)
  | Ebinop (op, e1, e2) -> () (* failwith "TODO" *)
  | Enot e -> () (* failwith "TODO" *)
  | Econdition (e1, e2, e3) -> () (* failwith "TODO" *)
  | Edesignator d -> () (* failwith "TODO" *)
  | Econst i32 -> () (* failwith "TODO" *)
  | Efuncall (id, el) -> () (* failwith "TODO" *)
  | Eerror s -> () (* failwith "TODO" *)
  | Emultiset_count (id, d, e) -> () (* failwith "TODO" *)
  | Eismem (d, te) -> () (* failwith "TODO" *)
  | Eisundef d -> () (* failwith "TODO" *)
      
and compile_exprs el =
  List.map compile_expr el

and compile_type_expr = function 
| Tident (id) -> () (* failwith "TODO" *)
| Tsubrange (i1, i2) -> () (* failwith "TODO" *)
| Tenum (idl) -> () (* failwith "TODO" *)
| Trecord (vdl) -> () (* failwith "TODO" *)
| Tarray (te1, te2) -> () (* failwith "TODO" *)
| Tscalarset i -> () (* failwith "TODO" *)
| Tunion te -> () (* failwith "TODO" *)
| Tmultiset (e, te) -> () (* failwith "TODO" *)
| Tint -> () (* failwith "TODO" *)
| Tany -> () (* failwith "TODO" *)

and compile_type_exprs tel =
  List.map compile_type_expr tel

let compile_proc_decl var = match var with
| _ -> () (* failwith "TODO" *)

let compile_proc_decls pdl =
  List.map compile_proc_decl pdl

let rec compile_rule rule =
  match rule.node with
  | Rsimple (os, e, dl, sl) -> () (* failwith "TODO" *)
  | Rstart (os, dl, sl) -> () (* failwith "TODO" *)
  | Rinvariant (os, e) -> () (* failwith "TODO" *)
  | Rruleset (ql, rl) -> () (* failwith "TODO" *)
  | Ralias (al, rl) -> () (* failwith "TODO" *)
  | Rchoose (id, d, rl) -> () (* failwith "TODO" *)

and compile_rules rl =
    List.map compile_rule rl

and compile_type_decl dtypes id = function
      | Tenum idl ->
          (id.node, List.map (fun e -> e.node) idl) :: dtypes
      | _ -> dtypes

      
and compile_decls dl =
      List.fold_left (
      fun (dvars, dtypes) d ->
        match d with 
        | Ast.Dtype (id, te) ->
            dvars, compile_type_decl dtypes id te
        | Ast.Dvar (id, te) ->
            compile_var dvars id.node [] te, dtypes
    ) (nop, []) dl

    


and string_of_type = function
| Tident tid -> tid.node
| Tscalarset _ -> "proc"
| Tsubrange _ -> "integer"
| Tunion te -> assert false (* TODO *)
| Tmultiset (e, te) -> assert false (* TODO *)
| Tarray _ | Trecord _ | Tenum _ | Tint 
| Tany -> failwith "Tany should not happen"

      
and compile_var decls id itl t =
    match t with
    | Tident tid ->
        decls ++ decl_l [Dglobal (id, tid.node)]
    | Trecord m -> compile_record_var decls id itl m
    | Tarray (te1, te2) ->
        begin match te2 with
        | Trecord m -> compile_record_array decls id (itl) te1 m
        | Tarray _ -> compile_var decls id ("proc"::itl) te2
        | _ -> decls ++ decl_l [Darray (id, (List.rev ("proc"::itl), string_of_type te2))]
        end
    | Tscalarset _ ->
        decls ++ decl_l [Dglobal (id, string_of_type t)]
    | Tsubrange _ ->
        decls ++ decl_l [Dglobal (id, string_of_type t)]
    | Tunion te ->
        nop  (* TODO *)
        (* decls ++ *)
    | Tmultiset (e, te) ->
        nop (* TODO *)
        (* decls ++ *)
    | Tenum _ -> failwith "Tenum should not happpen"


    | Tint -> failwith "todo"
    | Tany -> failwith "Tany should not happen"

and compile_record_array decls idv itl tindex m =
    StrMap.fold (fun idm t acc ->
      let new_id = (idv ^ "_" ^ idm) in
      match t with
      | Trecord m -> compile_record_array acc new_id itl tindex m    
      | Tscalarset _ | Tident _ | Tarray _ | Tunion _ | Tsubrange _
      | Tmultiset _ | Tenum _ | Tint | Tany -> 
          compile_var acc new_id itl (Tarray (tindex, t))
    ) m decls 
        
and compile_record_var decls idv itl m =
    StrMap.fold (fun idm t acc ->
      let new_id = (idv ^ "_" ^ idm) in
      match t with
      | Trecord m ->
          compile_record_var acc new_id itl m 
      | Tscalarset _ | Tident _ | Tarray _ | Tunion _ | Tsubrange _
      | Tmultiset _ | Tenum _ | Tint | Tany -> 
          compile_var acc new_id itl t
    ) m decls 
      

    
let compile_prog (p : Ast.type_expr Ast.prog) : Cub.system =
  Hashtbl.add types "boolean"
    (Tenum [loc_dummy "True"; loc_dummy "False"]);
  let dl, pfdl, rl = p in
  let cvdl, ctdl = compile_decls dl in
  let _ = compile_proc_decls pfdl in
  let _ = compile_rules rl in
  {
    type_defs = List.rev ctdl;
    decls = cvdl;
    init = (None, SAtom.empty);
    invs = [];
    cands = [];
    unsafe = [];
    forward = [];
    trans = []
  }




